1  /-
  2  Copyright (c) 2019 Scott Morrison. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Scott Morrison
  5  -/
  6  import algebra.category.Mon.basic
src         └────────────────────────┘
  7  import category_theory.limits.limits
src         └───────────────────────────┘
  8  
  9  /-!
 10  # The category of monoids has all colimits.
 11  
 12  We do this construction knowing nothing about monoids.
 13  In particular, I want to claim that this file could be produced by a python script
 14  that just looks at the output of `#print monoid`:
 15  
 16    -- structure monoid : Type u → Type u
 17    -- fields:
 18    -- monoid.mul : Π {α : Type u} [c : monoid α], α → α → α
 19    -- monoid.mul_assoc : ∀ {α : Type u} [c : monoid α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
 20    -- monoid.one : Π (α : Type u) [c : monoid α], α
 21    -- monoid.one_mul : ∀ {α : Type u} [c : monoid α] (a : α), 1 * a = a
 22    -- monoid.mul_one : ∀ {α : Type u} [c : monoid α] (a : α), a * 1 = a
 23  
 24  and if we'd fed it the output of `#print comm_ring`, this file would instead build
 25  colimits of commutative rings.
 26  
 27  A slightly bolder claim is that we could do this with tactics, as well.
 28  
 29  Because this file is "pre-automated", it doesn't meet current documentation standards.
 30  Hopefully eventually most of it will be automatically synthesised.
 31  -/
 32  
 33  universes v
 34  
 35  open category_theory
 36  open category_theory.limits
 37  
 38  namespace Mon.colimits
 39  
 40  variables {J : Type v} [small_category J] (F : J ⥤ Mon.{v})
id                           └────────────┘            └─┘
src                          └────────────┘            └─┘
typ                          └────────────┘            └─┘
doc                          └────────────┘            └─┘
 41  
 42  inductive prequotient
 43  -- There's always `of`
 44  | of : Π (j : J) (x : F.obj j), prequotient
id                          └──┘ 
src                         └──┘
typ                         └──┘ 
 45  -- Then one generator for each operation
 46  | one {} : prequotient
 47  | mul : prequotient → prequotient → prequotient
 48  
 49  open prequotient
 50  
 51  inductive relation : prequotient F → prequotient F → Prop
id                        └─────────┘     └─────────┘
src                       └─────────┘     └─────────┘
typ                       └─────────┘     └─────────┘
 52  -- Make it an equivalence relation:
 53  | refl : Π (x), relation x x
id                            
typ                           
 54  | symm : Π (x y) (h : relation x y), relation y x
id                       └──────┘               
typ                      └──────┘               
 55  | trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
id                         └──────┘         └──────┘               
typ                        └──────┘         └──────┘               
 56  -- There's always a `map` relation
 57  | map : Π (j j' : J) (f : j ⟶ j') (x : F.obj j), relation (of j' ((F.map f) x)) (of j x)
id                               └┘        └──┘              └┘ └┘    └──┘       └┘  
src                                         └──┘               └┘       └──┘         └┘
typ                              └┘        └──┘              └┘ └┘    └──┘       └┘  
 58  -- Then one relation per operation, describing the interaction with `of`
 59  | mul : Π (j) (x y : F.obj j), relation (of j (x * y)) (mul (of j x) (of j y))
id                        └──┘              └┘         └─┘  └┘     └┘  
src                        └──┘               └┘            └─┘  └┘       └┘
typ                       └──┘              └┘         └─┘  └┘     └┘  
 60  | one : Π (j), relation (of j 1) one
id                           └┘     └─┘
src                           └┘      └─┘
typ                          └┘     └─┘
 61  -- Then one relation per argument of each operation
 62  | mul_1 : Π (x x' y) (r : relation x x'), relation (mul x y) (mul x' y)
id                 └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
src                                                      └─┘       └─┘
typ                └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
 63  | mul_2 : Π (x y y') (r : relation y y'), relation (mul x y) (mul x y')
id                  └┘       └──────┘  └┘             └─┘     └─┘  └┘
src                                                      └─┘       └─┘
typ                 └┘       └──────┘  └┘             └─┘     └─┘  └┘
 64  -- And one relation per axiom
 65  | mul_assoc : Π (x y z), relation (mul (mul x y) z) (mul x (mul y z))
id                                   └─┘  └─┘       └─┘   └─┘  
src                                     └─┘  └─┘          └─┘    └─┘
typ                                  └─┘  └─┘       └─┘   └─┘  
 66  | one_mul : Π (x), relation (mul one x) x
id                               └─┘ └─┘   
src                               └─┘ └─┘
typ                              └─┘ └─┘   
 67  | mul_one : Π (x), relation (mul x one) x
id                               └─┘  └─┘  
src                               └─┘   └─┘
typ                              └─┘  └─┘  
 68  
 69  def colimit_setoid : setoid (prequotient F) :=
id                        └────┘  └─────────┘ 
src                       └────┘  └─────────┘
typ                       └────┘  └─────────┘ 
 70  { r := relation F, iseqv := ⟨relation.refl, relation.symm, relation.trans⟩ }
id          └──────┘             └───────────┘  └───────────┘  └────────────┘
src         └──────┘              └───────────┘  └───────────┘  └────────────┘
typ         └──────┘             └───────────┘  └───────────┘  └────────────┘
 71  attribute [instance] colimit_setoid
id                        └────────────┘
src                       └────────────┘
typ                       └────────────┘
 72  
 73  def colimit_type : Type v := quotient (colimit_setoid F)
id                                └──────┘  └────────────┘ 
src                               └──────┘  └────────────┘
typ                               └──────┘  └────────────┘ 
 74  
 75  instance monoid_colimit_type : monoid (colimit_type F) :=
 76  { mul :=
 77    begin
 78      fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id               └───────┘       └──────────┘       └──────────┘ 
src      └─────┘          └───┘               └┘  └──────────┘ └┘
typ      └─────┘ └───────┘└───┘  └──────────┘ └┘  └──────────┘└┘
doc      └─────┘          └───┘               └┘               └┘
txt      └─────┘          └───┘               └┘               └┘
par      └─────┘          └───┘               └┘               └┘
pid                      └───┘               └┘               └┘
st             └───────────────────────────────────────────────────┘└─
 79      { intro x,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ─────┘└─────┘└─
 80        fapply @quot.lift,
id                 └───────┘
src        └─────┘
typ        └─────┘ └───────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid              
st   ──────────────────────┘└─
 81        { intro y,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
pid               └┘
st   ───────┘└─────┘└─
 82          exact quot.mk _ (mul x y) },
id                 └─────┘    └─┘  
src          └────┘       └─┘ └─┘  └┘
typ          └────┘└─────┘└─┘ └─┘└┘
doc          └────┘       └─┘      └┘
txt          └────┘       └─┘      └┘
par          └────┘       └─┘      └┘
pid                      └─┘      
st   ─────────────────────────────────┘└┘
 83        { intros y y' r,
src          └───────────┘
typ          └───────────┘
doc          └───────────┘
txt          └───────────┘
par          └───────────┘
pid                └─────┘
st   ────────────────────┘└─
 84          apply quot.sound,
id                 └────────┘
src          └────┘└────────┘
typ          └────┘└────────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────────────────────┘└─
 85          exact relation.mul_2 _ _ _ r } },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ────────────────────────────────────┘└──┘
 86      { intros x x' r,
src        └───────────┘
typ        └───────────┘
doc        └───────────┘
txt        └───────────┘
par        └───────────┘
pid              └─────┘
st   ──────────────────┘└─
 87        funext y,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid              └┘
st   ─────────────┘└─
 88        induction y,
id                   
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid                 
st   ────────────────┘└─
 89        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
 90        apply quot.sound,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
 91        { exact relation.mul_1 _ _ _ r },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ───────┘└───────────────────────────┘└┘
 92        { refl } },
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
pid              
st   ────────────┘└────
 93    end,
st   ────┘
 94    one :=
 95    begin
st     └─────
 96      exact quot.mk _ one
id             └─────┘   └─┘
src      └────┘       └─┘└─┘
typ      └────┘└─────┘└─┘└─┘
doc      └────┘       └─┘   
txt      └────┘       └─┘   
par      └────┘       └─┘   
pid                  └─┘   
st   ────────────────────────
 97    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 98    mul_assoc := λ x y z,
id                      
typ                     
 99    begin
st     └─────
100      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
101      induction y,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
102      induction z,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
103      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
104      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
105      apply relation.mul_assoc,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────┘└─
106      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
107      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
108      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
109    end,
st   ────┘
110    one_mul := λ x,
id                  
typ                 
111    begin
st     └─────
112      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
113      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
114      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
115      apply relation.one_mul,
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────┘└─
116      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
117    end,
st   ────┘
118    mul_one := λ x,
id                  
typ                 
119    begin
st     └─────
120      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
121      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
122      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
123      apply relation.mul_one,
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────┘└─
124      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
125    end }
st   ────┘
126  
127  @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl
id                            └─────┘ └──────┘ └─┘       └──────────┘      └─┘
src                                   └──────┘ └─┘       └──────────┘       └─┘
typ                           └─────┘ └──────┘ └─┘       └──────────┘      └─┘
doc    └──┘
128  @[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
id                                  └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
src                                         └──────┘  └─┘                 └──────┘              └──────┘      └──────────┘       └─┘
typ                                 └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
doc    └──┘
129  
130  def colimit : Mon := ⟨colimit_type F, by apply_instance⟩
id                 └─┘     └──────────┘ 
src                └─┘     └──────────┘       └────────────┘
typ                └─┘     └──────────┘      └────────────┘
doc                └─┘                        └────────────┘
txt                                           └────────────┘
par                                           └────────────┘
st                                           └─────────────┘
131  
132  def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
id                              └──┘     └──────────┘ 
src                               └──┘      └──────────┘
typ                             └──┘     └──────────┘ 
133  quot.mk _ (of j x)
id   └─────┘    └┘  
src             └┘
typ  └─────┘    └┘  
134  
135  def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
id                                └──┘   └─────┘ 
src                                 └──┘    └─────┘
typ                               └──┘   └─────┘ 
136  { to_fun := cocone_fun F j,
id               └────────┘  
src              └────────┘
typ              └────────┘  
137    map_one' := quot.sound (relation.one _ _),
id                 └────────┘  └──────────┘
src                └────────┘  └──────────┘
typ                └────────┘  └──────────┘
138    map_mul' := λ x y, quot.sound (relation.mul _ _ _) }
id                      └────────┘  └──────────┘
src                       └────────┘  └──────────┘
typ                     └────────┘  └──────────┘
139  
140  @[simp] lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
id                                                    └┘
src                                                    
typ                                                   └┘
doc    └──┘
141    F.map f ≫ (cocone_morphism F j') = cocone_morphism F j :=
id     └──┘    └─────────────┘  └┘   └─────────────┘  
src     └──┘     └─────────────┘        └─────────────┘
typ    └──┘    └─────────────┘  └┘   └─────────────┘  
142  begin
st   └─────
143    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
144    apply quot.sound,
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────┘└─
145    apply relation.map,
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────┘└─
146  end
st   ──┘
147  
148  @[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j):
id                                                               └┘       └──┘ 
src                                                                          └──┘
typ                                                              └┘       └──┘ 
doc    └──┘
149    (cocone_morphism F j') (F.map f x) = (cocone_morphism F j) x :=
id      └─────────────┘  └┘   └──┘      └─────────────┘    
src     └─────────────┘         └──┘        └─────────────┘
typ     └─────────────┘  └┘   └──┘      └─────────────┘    
150  by { rw ←cocone_naturality F f, refl }
id            └───────────────┘  
src       └──┘└───────────────┘    └───┘
typ       └──┘└───────────────┘  └───┘
doc       └──┘                     └───┘
txt       └──┘                     └───┘
par       └──┘                     └───┘
pid         └┘                         
st     └──────────────────────────┘└─────┘└┘
151  
152  def colimit_cocone : cocone F :=
id                        └────┘ 
src                       └────┘
typ                       └────┘ 
doc                       └────┘
153  { X := colimit F,
id          └─────┘ 
src         └─────┘
typ         └─────┘ 
154    ι :=
155    { app := cocone_morphism F, } }.
id             └─────────────┘ 
src            └─────────────┘
typ            └─────────────┘ 
doc    
156  
157  @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
id                                  └────┘     └─────────┘   └┘
src                                 └────┘      └─────────┘      └┘
typ                                 └────┘     └─────────┘   └┘
doc    └──┘                         └────┘
158  | (of j x)  := (s.ι.app j) x
id      └┘         └┘└──┘
src     └┘            └┘└──┘
typ     └┘         └┘└──┘
159  | one       := 1
id     └─┘
src    └─┘
typ    └─┘
160  | (mul x y) := desc_fun_lift x * desc_fun_lift y
id      └─┘       └───────────┘    └───────────┘
src     └─┘                         
typ     └─┘       └───────────┘    └───────────┘
161  
162  def desc_fun (s : cocone F) : colimit_type F → s.X :=
id                     └────┘     └──────────┘    └┘
src                    └────┘      └──────────┘      └┘
typ                    └────┘     └──────────┘    └┘
doc                    └────┘
163  begin
st   └─────
164    fapply quot.lift,
id            └───────┘
src    └─────┘
typ    └─────┘└───────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid          
st   ─────────────────┘└─
165    { exact desc_fun_lift F s },
id             └───────────┘  
src      └────┘└───────────┘  
typ      └────┘└───────────┘
doc      └────┘               
txt      └────┘               
par      └────┘               
pid                          
st   ───┘└──────────────────────┘└┘
166    { intros x y r,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid            └────┘
st   ───────────────┘└─
167      induction r; try { dsimp },
id                 
src      └────────┘   └────┘└────┘
typ      └────────┘  └────┘└────┘
doc      └────────┘   └────┘└────┘
txt      └────────┘   └────┘└────┘
par      └────────┘   └────┘└────┘
pid                     └────────┘
st   ─────────────────────┘└─────┘└┘
168      -- refl
st   ────────────
169      { refl },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
170      -- symm
st   ────────────
171      { exact r_ih.symm },
id               └───────┘
src        └────┘└───────┘
typ        └────┘└───────┘
doc        └────┘         
txt        └────┘         
par        └────┘         
pid                      
st   ─────┘└──────────────┘└┘
172      -- trans
st   ─────────────
173      { exact eq.trans r_ih_h r_ih_k },
id               └──────┘ └────┘ └────┘
src        └────┘└──────┘            
typ        └────┘└──────┘└────┘└────┘
doc        └────┘                    
txt        └────┘                    
par        └────┘                    
pid                                 
st   ─────┘└───────────────────────────┘└┘
174      -- map
st   ───────────
175      { rw cocone.naturality_concrete, },
id            └────────────────────────┘
src        └─┘└────────────────────────┘
typ        └─┘└────────────────────────┘
doc        └─┘└────────────────────────┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└───────────────────────────┘└──┘
176      -- mul
st   ───────────
177      { rw is_monoid_hom.map_mul ⇑((s.ι).app r_j) },
id            └───────────────────┘   └─┘      └─┘
src        └─┘└───────────────────┘  └─┘└────┘   └┘
typ        └─┘└───────────────────┘  └─┘└────┘└─┘└┘
doc        └─┘└───────────────────┘      └────┘   └┘
txt        └─┘                           └────┘   └┘
par        └─┘                           └────┘   └┘
pid                                     └────┘   
st   ─────┘└────────────────────────────────────────┘└┘
178      -- one
st   ───────────
179      { erw is_monoid_hom.map_one ⇑((s.ι).app r), refl },
id             └───────────────────┘    └─┘      
src        └──┘└───────────────────┘   └─┘└────┘   └───┘
typ        └──┘└───────────────────┘   └─┘└────┘  └───┘
doc        └──┘                           └────┘   └───┘
txt        └──┘                           └────┘   └───┘
par        └──┘                           └────┘   └───┘
pid                                      └────┘       
st   ─────┘└──────────────────────────────────────┘└─────┘└┘
180      -- mul_1
st   ─────────────
181      { rw r_ih, },
id            └──┘
src        └─┘
typ        └─┘└──┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└─────┘└──┘
182      -- mul_2
st   ─────────────
183      { rw r_ih, },
id            └──┘
src        └─┘
typ        └─┘└──┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└─────┘└──┘
184      -- mul_assoc
st   ─────────────────
185      { rw mul_assoc, },
id            └───────┘
src        └─┘└───────┘
typ        └─┘└───────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└──────────┘└──┘
186      -- one_mul
st   ───────────────
187      { rw one_mul, },
id            └─────┘
src        └─┘└─────┘
typ        └─┘└─────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└────────┘└──┘
188      -- mul_one
st   ───────────────
189      { rw mul_one, } }
id            └─────┘
src        └─┘└─────┘
typ        └─┘└─────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ───────────────┘└─────
190  end
st   ──┘
191  
192  @[simp] def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
id                                  └────┘     └─────┘   └┘
src                                 └────┘      └─────┘     └┘
typ                                 └────┘     └─────┘   └┘
doc    └──┘                         └────┘
193  { to_fun := desc_fun F s,
id               └──────┘  
src              └──────┘
typ              └──────┘  
194    map_one' := rfl,
id                 └─┘
src                └─┘
typ                └─┘
195    map_mul' := λ x y, by { induction x; induction y; refl }, }
id                                                 
src                            └────────┘   └────────┘   └───┘
typ                          └────────┘  └────────┘  └───┘
doc                            └────────┘   └────────┘   └───┘
txt                            └────────┘   └────────┘   └───┘
par                            └────────┘   └────────┘   └───┘
pid                                                        
st                          └────────────────────────────────┘└┘
196  
197  def colimit_is_colimit : is_colimit (colimit_cocone F) :=
id                            └────────┘  └────────────┘ 
src                           └────────┘  └────────────┘
typ                           └────────┘  └────────────┘ 
doc                           └────────┘
198  { desc := λ s, desc_morphism F s,
id                └───────────┘  
src                └───────────┘
typ               └───────────┘  
doc  
199    uniq' := λ s m w,
id                  
typ                 
200    begin
st     └─────
201      ext,
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
st   ──────┘└─
202      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
203      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
204      { have w' := congr_fun (congr_arg (λ f : F.obj x_j ⟶ s.X, (f : F.obj x_j → s.X)) (w x_j)) x_x,
id                    └───────┘  └───────┘        └───┘                └───┘       └─┘     └─┘   └─┘
src        └─────────┘└───────┘ └───────┘  └───┘           └┘  └─┘└───┘    └─┘└─┘     └─┘
typ        └─────────┘└───────┘ └───────┘  └───┘└───┘      └┘  └─┘└───┘    └─┘└─┘ └─┘└─┘└─┘
doc        └─────────┘                     └───┘            └┘  └─┘            └─┘     └─┘
txt        └─────────┘                     └───┘            └┘  └─┘            └─┘     └─┘
par        └─────────┘                     └───┘            └┘  └─┘            └─┘     └─┘
pid        └─────┘└─┘                     └───┘            └┘  └─┘            └─┘     └─┘
st   ─────┘└─────────────────────────────────────────────────────────────────────────────────────────┘└─
205        erw w',
id             └┘
src        └──┘
typ        └──┘└┘
doc        └──┘
txt        └──┘
par        └──┘
pid           
st   ───────────┘└─
206        refl, },
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────────┘└──┘
207      { simp only [desc_morphism, quot_one],
id                    └───────────┘  └──────┘
src        └─────────┘└───────────┘└┘└──────┘
typ        └─────────┘└───────────┘└┘└──────┘
doc        └─────────┘             └┘        
txt        └─────────┘             └┘        
par        └─────────┘             └┘        
pid            └──┘└┘             └┘        
st   ─────┘└─────────────────────────────────┘└─
208        erw is_monoid_hom.map_one ⇑m,
id             └───────────────────┘ 
src        └──┘└───────────────────┘
typ        └──┘└───────────────────┘
doc        └──┘                     
txt        └──┘                     
par        └──┘                     
pid                                
st   ─────────────────────────────────┘└─
209        refl, },
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────────┘└──┘
210      { simp only [desc_morphism, quot_mul],
id                    └───────────┘  └──────┘
src        └─────────┘└───────────┘└┘└──────┘
typ        └─────────┘└───────────┘└┘└──────┘
doc        └─────────┘             └┘        
txt        └─────────┘             └┘        
par        └─────────┘             └┘        
pid            └──┘└┘             └┘        
st   ─────┘└─────────────────────────────────┘└─
211        erw is_monoid_hom.map_mul ⇑m,
id             └───────────────────┘  
src        └──┘└───────────────────┘
typ        └──┘└───────────────────┘ 
doc        └──┘└───────────────────┘
txt        └──┘                     
par        └──┘                     
pid                                
st   ─────────────────────────────────┘└─
212        rw [x_ih_a, x_ih_a_1],
id             └────┘  └──────┘
src        └──┘      └┘        
typ        └──┘└────┘└┘└──────┘
doc        └──┘      └┘        
txt        └──┘      └┘        
par        └──┘      └┘        
pid          └┘      └┘        
st   ───────────────┘└────────┘└─
213        refl, },
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────────┘└──┘
214      refl
src      └────
typ      └────
doc      └────
txt      └────
par      └────
pid          
st   ─────────
215    end }.
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
216  
217  instance has_colimits_Mon : has_colimits.{v} Mon.{v} :=
id                               └──────────┘     └─┘
src                              └──────────┘     └─┘
typ                              └──────────┘     └─┘
doc                              └──────────┘     └─┘
218  { has_colimits_of_shape := λ J 𝒥,
id                                 
typ                                
219    { has_colimit := λ F, by exactI
id                        
src                             └──────
typ                            └──────
doc                             └──────
txt                             └──────
par                             └──────
pid                                   
st                             └───────
220      { cocone := colimit_cocone F,
id                   └────────────┘
src  ───┘ └─────────┘└────────────┘ └─
typ  ───┘ └─────────┘└────────────┘ └─
doc  ───┘ └─────────┘               └─
txt  ───┘ └─────────┘               └─
par  ───┘ └─────────┘               └─
pid  ───┘ └─────────┘               └─
st   ──────────────────────────────────
221        is_colimit := colimit_is_colimit F } } }
id                       └────────────────┘ 
src  ───────────────────┘└────────────────┘ └─┘
typ  ───────────────────┘└────────────────┘└─┘
doc  ───────────────────┘                   └─┘
txt  ───────────────────┘                   └─┘
par  ───────────────────┘                   └─┘
pid  ───────────────────┘                   └┘
st   ──────────────────────────────────────────┘
222  
223  end Mon.colimits